$\forall$${\it es}$:event\_system\{i:l\}, $i$,$x$:Id, $T$:Type.
\\[0ex]es{-}dtype(${\it es}$; $i$; $x$; $T$)
\\[0ex]$\Rightarrow$ ($\forall$$t$:rationals. es{-}init{-}elapsed(${\it es}$; $i$; $t$)($x$) = es{-}initially(${\it es}$; $i$; $x$) $\in$ $T$)